# Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
#
# SPDX-License-Identifier: CC-BY-SA-4.0
#

@book{Nipkow_PW:Isabelle,
  author    = {Tobias Nipkow and Lawrence Paulson and Markus Wenzel},
  title     = {{Isabelle/HOL} --- A Proof Assistant for Higher-Order Logic},
  publisher = sv,
  series    = lncs,
  volume    = 2283,
  year      = 2002,
  doi       = {10.1007/3-540-45949-9},
  isbn      = {978-3-540-43376-7},
}

  @techreport{Fernandez_KKM_13:tr,
    issn             = {1833-9646-7650},
    institution      = {NICTA and UNSW},
    author           = {Fernandez, Matthew and Klein, Gerwin and Kuz, Ihor and Murray, Toby},
    format           = {pdf},
    month            = nov,
    year             = {2013},
    title            = {{CAmkES} Formalisation of a Component Platform},
    type             = {Technical Report},
    address          = {Australia}
  }

  @techreport{Fernandez_GAKK_13:tr,
    issn             = {1833-9646-7633},
    institution      = {NICTA and UNSW},
    author           = {Fernandez, Matthew and Gammie, Peter and Andronick, June and Klein, Gerwin and Kuz, Ihor},
    format           = {pdf},
    month            = nov,
    year             = {2013},
    title            = {{CAmkES} Glue Code Semantics},
    type             = {Technical Report},
    address          = {Australia}
  }

  @inproceedings{Greenaway_LAK_14,
    author           = {Greenaway, David and Lim, Japheth and Andronick, June and Klein, Gerwin},
    format           = {pdf},
    month            = jun,
    year             = {2014},
    title            = {Don't Sweat the Small Stuff: Formal Verification of C Code Without the Pain},
    type             = {Conference Paper},
    booktitle        = pldi,
    address          = {Edinburgh, UK}
  }

  @inproceedings{Winwood_KSACN_09,
    publisher        = sv,
    series           = lncs,
    format           = {pdf},
    author           = {Simon Winwood and Gerwin Klein and Thomas Sewell and June Andronick and David Cock and Michael
                        Norrish},
    month            = aug,
    volume           = {5674},
    editor           = {Stefan Berghofer and Tobias Nipkow and Christian Urban and Makarius Wenzel},
    year             = {2009},
    title            = {Mind the Gap: A Verification Framework for Low-Level {C}},
    booktitle        = tphols09,
    pages            = {500--515},
    address          = {Munich, Germany}
  }

  @article{Kuz_LGH_07,
    author           = {Ihor Kuz and Yan Liu and Ian Gorton and Gernot Heiser},
    title            = {{CAmkES}: A component model for secure microkernel-based embedded systems},
    journal          = {Journal of Systems and Software Special Edition on Component-Based Software Engineering of
                        Trustworthy Embedded Systems},
    format           = {http://dx.doi.org/10.1016/j.jss.2006.08.039},
    year             = 2007,
    number           = {5},
    month            = may,
    volume           = {80},
    htmlnote         = {<a href="/publications/papers/Kuz_LGH_07.pdf">Preprint</a>},
    pages            = {687--699}
  }

  @inproceedings{Klein_EHACDEEKNSTW_09,
    publisher        = acmpress,
    doi              = {10.1145/1629575.1629596},
    author           = {Gerwin Klein and Kevin Elphinstone and Gernot Heiser and June Andronick and David Cock and Philip
                        Derrin and Dhammika Elkaduwe and Kai Engelhardt and Rafal Kolanski and Michael Norrish and Thomas
                        Sewell and Harvey Tuch and Simon Winwood},
    format           = {pdf},
    year             = {2009},
    month            = oct,
    video            = {http://www.sigops.org/sosp/sosp09/videos/15_gerwin_klein.mov},
    htmlnote         = {<span class="important">Best Paper Award!</span>},
    title            = {{seL4}: Formal Verification of an {OS} Kernel},
    booktitle        = sosp09,
    pages            = {207--220},
    address          = {Big Sky, MT, USA}
  }

@techreport{C99,
  author={{ISO/IEC}},
  title={Programming languages --- {C}},
  number={9899:TC2},
  institution={ISO/IEC JTC1/SC22/WG14},
  month=May,
  year=2005,
}

